module AbsSupportRust where

import AbsRust
import PrintRust
import EnvRust

--restituisce un errore di tipo nel caso in cui il cast non sia valido,
--altrimenti restituisce il primo argomento
castType :: Type -> Type -> Position -> String -> Type
castType t (TErr _) _ _ = t
castType t@(BasicType BTChar) t1 pos err = case t1 of
   BasicType BTChar -> t
   BasicType BTInt -> t
   BasicType BTFloat -> t
   _ -> TErr $ pos++" invalid cast from type "++printTree t1++" to type "++printTree t++err

castType t@(BasicType BTInt) t1 pos err = case t1 of
   BasicType BTFloat -> t
   Pointer _ -> t
   _ -> meetType t t1 pos err

castType t@(BasicType BTFloat) t1 pos err = meetType t t1 pos err
castType t@(Pointer _) (BasicType BTInt) _ _ = t
castType t1 t2 pos err = meetTypeRigid t1 t2 pos err

--calcola il massimo tra i due tipi dati in input, oppure un type error nel caso 
-- in cui i tipi non siano compatibili
maxType :: Type -> Type -> Position -> Type
maxType t@(BasicType BTChar) t2 pos = case t2 of
   BasicType BTInt -> t2
   BasicType BTFloat -> t2
   _ -> meetTypeRigid t t2 pos ".\n" 

maxType t@(BasicType BTInt) t2 pos = case t2 of
   BasicType BTChar -> t
   BasicType BTFloat -> t2
   _ -> meetTypeRigid t t2 pos ".\n"

maxType t@(BasicType BTFloat) t2 pos = case t2 of
   BasicType BTChar -> t
   BasicType BTInt -> t
   _ -> meetTypeRigid t t2 pos ".\n"
maxType t t2 pos = meetTypeRigid t t2 pos ".\n"

-- controlla che i tipi in input siano uguali, altrimenti genera un errore di tipo
meetTypeRigid :: Type -> Type -> Position -> String -> Type
meetTypeRigid (TErr _) (TErr _) pos err = TErr $ pos++" invalid types"++err
meetTypeRigid (TErr _) t _ _ = t
meetTypeRigid t (TErr _) _ _ = t
meetTypeRigid a1@(Array n t) a2@(Array m t') pos err
   | n /= m = TErr $ pos++" incompatible array dimension: "++printTree a1++" and "++printTree a2++".\n"
   | otherwise = Array n $ meetTypeRigid t t' pos err
meetTypeRigid t1 t2 pos err
   |t1 == t2 = t1
   |otherwise = TErr $ pos++" provided incompatible types "++printTree t1++" and "++printTree t2++err

--determina se sia valida la coertion al primo tipo del secondo,
-- in caso contrario genera un errore di tipo
meetType :: Type -> Type -> Position -> String -> Type
meetType t@(BasicType BTChar) t2 pos err = meetTypeRigid t t2 pos err
meetType t@(BasicType BTInt) t2 pos err = case t2 of
   BasicType BTChar -> t
   _ -> meetTypeRigid t t2 pos err

meetType t@(BasicType BTFloat) t2 pos err = case t2 of
   BasicType BTChar -> t
   BasicType BTInt -> t
   _ -> meetTypeRigid t t2 pos err

meetType a1@(Array Nothing t) a2@(Array _ t') pos err = Array Nothing $ meetTypeRigid t t' pos err
meetType t t2 pos err = meetTypeRigid t t2 pos err

--effettua la coertion al primo tipo del secondo
widenType :: Type -> Type -> RExpr -> RExpr
widenType t t1 e
   |t == t1 = e
   |otherwise = Coertion t t1 (e,t)

--controlla se la funzione main è presente tra gli item dichiarati
validProg :: [Item] -> Env -> (Program,Env)
validProg is env = case lookupFun env mainf initPath of
   [] -> (Prog is err,env)
   _ -> (Prog is "",env)
   where
      mainf = funIdent "main" []
      err = "Error: function main/0 is undefined.\n" 

--controlla se lo static item sia valido o meno, generando opportuni messaggi d'errore
validIStat :: Env -> Path -> Id -> Type -> (RExpr,Type) -> Position -> Item
validIStat e pat i t r@(re,te) pos = case lookupVar e i pat of
   [] -> IStat i (validInitStatic t te re pos initErr) r
   _ -> IStat i terr r
   where
      terr = TErr $ pos++" static variable \"" ++ printTree i ++ "\" has already been declared.\n"
      initErr = " in the definition of the static variable \""++printTree i++"\".\n"

--controlla se il tipo dello static item e la corrispondente rexpr siano corretti
--e se la rexpr sia valida
validInitStatic :: Type -> Type -> RExpr -> Position -> Error -> Type
validInitStatic t te re pos err = case meetTypeRigid t te pos e of
   TErr s -> TErr s
   _ -> validStaticRExpr t te re pos e
   where
      e = " in expression \""++printTree re++"\""++err

--controlla se la rexpr di inizializzazione dello static item sia composta solo di costanti,
--array di costanti, o tuple di costanti
validStaticRExpr :: Type -> Type -> RExpr -> Position -> Error -> Type
validStaticRExpr t te re pos err = case p re of
   True -> t
   _ -> TErr $ pos++ " only constant expression can be used to initialize a static variable,"++err
   where
      p (Const _) = True
      p (TRExpr ts) = foldr f True (reverse ts)
      p (ArrRExpr ts) = foldr f True (reverse ts)
      p _ = False
      f (re,_) b = p re && b

--controlla se la funzione risulta essere valida, controllando che il tipo di ritorno 
--del blocco sia corretto, che i parametri siano corretti e non duplicati, infine che la
--funzione non sia gia stata dichiarata nel corrente blocco
validIFun :: Env -> Path -> Id -> [Parameter] -> Type -> (Block,Type) -> Position -> Item
validIFun e pat i ps t (bk,tk) pos = case lookupFun e fi pat of
   [] -> item t
   fs -> aggr fs
   where
      item typ = IFun i (notTwiceParam pos ps) typ (checkBlock t tk bk pos err)
      fi = funIdent i ps 
      err = " in the return expression of the function "++ printTree i ++".\n"
      terr = TErr $ pos++" double declaration of function "++ printTree i ++".\n"
      f = funInfo ps t pat
      rs = filter (p f) 
      p (FI ps1 _ _ pt1) (FI ps2 _ _ pt2) = pt1 == pt2 && all (==True) (zipWith (==) ps1 ps2)
      aggr cs
         |null (rs cs) = item t
         |otherwise = item terr

notTwiceParam :: Position -> [Parameter] -> [Parameter]
notTwiceParam pos = snd . foldr f ([],[])
   where
      f p@(Param m v t) (pv,ps)
         |elem v pv == False = (v:pv,p:ps)
         |otherwise = (pv,pe:ps)
        where
            pe = Param m v (TErr $ pos++" double declaration of a parameter variable identifier, in "++printTree p++".\n")

checkBlock :: Type -> Type -> Block -> Position -> String -> (Block,Type)
checkBlock t tk b@(Block ss (re,te)) pos err = case t1 of
   TErr s -> (b,t1)
   _ -> (Block ss (r,te), t)
   where
      t1 = meetType t tk pos $ e++err
      e = " in expression \""++printTree re++"\""
      r = widenType tk t re

--determina se il let statement sia corretto, controllando che il tipo dell'espressione di inizializzazione,
--se presente, sia sottotipo del tipo della dichiarazione; inoltre controlla che i nomi
-- delle variabili siano unici all'interno del blocco
validLet :: Env -> Path -> Attribute -> Var -> Type -> (Maybe (RExpr,Type)) -> Position -> Stmt
validLet e pat att v t Nothing pos = Let att var tr Nothing
   where
      v1 = checkVar e pat pos v
      var = checkTwiceVar pos v1
      tr = validVarType pos v t

validLet e pat att v t (Just (re,te)) pos = Let att var tr (Just rs)
   where
      v1 = checkVar e pat pos v
      var = checkTwiceVar pos v1
      tr = validVarType pos v t
      rs = validInitVar pos err t te re
      err = " in the definition of variable \""++ printTree v ++"\".\n"

validVarType :: Position -> Var -> Type -> Type
validVarType pos (Var _ _) t = t
validVarType pos (VTup vs) (Tuple ts)
   |vn == tn = Tuple zs
   |otherwise = TErr $ pos++" the number of tuple elements ("++show vn++") differ from tuple type definition ("++show tn++").\n"
   where
      zs = zipWith (validVarType pos) vs ts
      vn = length vs
      tn = length ts
validVarType pos v@(VTup vs) t = TErr $ pos++" variable \""++printTree v++"\" is not defined as a tuple.\n" 

--controlla che la variabile non sia già presente all'interno dell'environment,
--altrimenti associa un messaggio di errore
checkVar :: Env -> Path -> Position -> Var -> Var
checkVar e pat pos (Var i _) = cVar e pat i pos
checkVar e pat pos (VTup vs) = (VTup (reverse rs))
   where
      rs = foldr ((:) . checkVar e pat pos) [] (reverse vs)
      
cVar :: Env -> Path -> Id -> Position -> Var
cVar e pat i pos = case lookupVar e i pat of
   [] ->  var
   vs -> aggr vs
   where
      var = Var i ""
      verr = Var i $ pos++" variable \""++ printTree i ++"\" has already been declared.\n"
      rs = filter (p pat)
      aggr cs
         |null (rs cs) = var
         |otherwise = verr
      p pt1 v2 = case v2 of
         (VStatic _ _ _) -> True
         (VPar _ _ pt2) -> pt1 == pt2
         (VVar _ pt2)  -> pt1 == pt2
         (VConst _ pt2) -> pt1 == pt2

--controlla che all'interno di una definizione di tuple, le variabili non siano dichiarate doppie,
--altrimenti associa in messaggio di errore
checkTwiceVar :: Position -> Var -> Var
checkTwiceVar pos v = var
   where
      ([var],_) = cTwiceVar pos v ([],[])

cTwiceVar pos v@(Var i err) (vars,ids)
   |elem i ids = (verr:vars,ids)
   |otherwise = (v:vars,i:ids)
   where
      verr = Var i $ pos++" double declaration of variable identifier "++i++".\n"++err

cTwiceVar pos (VTup vs) (vars,ids) = (vtup:vars,ids1)
   where
      (vtups,ids1) = foldr (cTwiceVar pos) ([],ids) (reverse vs)
      vtup = VTup (reverse vtups)

validInitVar :: Position -> Error -> Type -> Type -> RExpr -> (RExpr,Type)
validInitVar pos err t te re = case t1 of
   TErr s -> (r,t1)
   _ -> (r,t)
   where
      t1 = meetType t te pos $ e++err
      e = " in expression \""++printTree re++"\""
      r = widenType te t re

--determina la validita' dell'espressione di assegnamento controllando che il tipo della
--rexpr a destra dell'operatore di assegnamento sia minore o uguale al tipo dell'espressione di sinistra
validAssign :: AssignmentOp -> (RExpr, Type) -> (RExpr, Type) -> Position -> (RExpr, Type)
validAssign aOp l@(LExpr _,_) r pos = vAssign aOp l r pos
validAssign aOp l r pos = (e,terr)
   where
      e = Assgn aOp l r
      terr = TErr $ pos++" the left side of an assignment must be an lexpr\""++printTree e++"\".\n"

vAssign :: AssignmentOp -> (RExpr, Type) -> (RExpr, Type) -> Position -> (RExpr, Type)
vAssign Assign l@(l1,t1) re@(r1, t2) pos = (e,t1)
   where
      e = Assgn Assign l r
      err = Assgn Assign l re
      r = (widenType t2 t1 r1, tt)
      tt = meetType t1 t2 pos $ " in the right side of the assignment \""++printTree err++"\".\n"
      
vAssign (AssgnArith Pow) l@(l1,t1) re@(r1, t2) pos = (e,t')
   where
      e = Assgn (AssgnArith Pow) l r
      err = Assgn (AssgnArith Pow) l re
      t' = validArithOpType Pow t1 pos $ " in the left side of the assignment \""++printTree err++"\".\n"
      ti = BasicType BTInt
      t2' = meetType ti t2 pos $ " in the right side of the assignment \""++printTree err++ "\".\n"
      r = (widenType t2 ti r1, t2')

vAssign (AssgnArith Mod) l@(l1,t1) re@(r1, t2) pos = (e,t')
   where
      e = Assgn (AssgnArith Mod) l r
      err = Assgn (AssgnArith Mod) l re
      t' = validArithOpType Mod t1 pos $ " in the left side of the assignment \""++printTree err++"\".\n"
      ti = BasicType BTInt
      t2' = meetType ti t2 pos $ " in the right side of the assignment \""++printTree err++ "\".\n"
      r = (widenType t2 ti r1, t2')

vAssign (AssgnArith aOp) l@(l1,t1) re@(r1, t2) pos = (e,t')
   where
      e = Assgn (AssgnArith aOp) l r
      err = Assgn (AssgnArith aOp) l re
      t' = validArithOpType aOp t1 pos $ " in the left side of the assignment \""++printTree err++"\".\n"
      t = meetType t1 t2 pos $ " in the right side of the assignment \""++printTree err++ "\".\n"
      r = (widenType t2 t1 r1, t)

vAssign (AssgnBool bOp) l@(l1,t1) re@(r2,t2) pos= (e,tb)
   where
      e = Assgn (AssgnBool bOp) l' r'
      err = Assgn (AssgnBool bOp) l re
      tb = BasicType BTBool
      r' = (widenType t2 tb r2, t')
      l' = (widenType t1 tb l1, t)
      t' = meetTypeRigid tb t2 pos $ " in the left side of the assignment \""++printTree err++"\".\n"
      t = meetTypeRigid tb t1 pos $ " in the right side of the assignment \""++printTree err++ "\".\n"

validArithOpType :: ArithOp -> Type -> Position -> String -> Type
validArithOpType Pow t@(BasicType BTChar) pos err = TErr $ pos++" invalid type "++printTree t++" for operator "++printTree Pow++err
validArithOpType aOp t@(BasicType BTChar) _ _ = t
validArithOpType aOp t@(BasicType BTInt) _ _ = t
validArithOpType aOp t@(BasicType BTFloat) _ _ = t
validArithOpType aOp t p s = TErr $ p++" invalid type "++printTree t++" for operator "++printTree aOp++ s

validUnaryOpType :: UnaryOp -> Type -> Position -> String -> Type
validUnaryOpType Not t@(BasicType BTBool) _  _= t
validUnaryOpType Neg t@(BasicType BTChar) _  _= t
validUnaryOpType Neg t@(BasicType BTInt) _  _= t
validUnaryOpType Neg t@(BasicType BTFloat) _  _= t
validUnaryOpType uOp t pos err = TErr $ pos ++" invalid type "++printTree t++" for operator "++printTree uOp++err

--determina se l'espressione è valida controllando che i tipi siano validi per l'operatore
-- ed effettua, se necessario, una coertion del tipo
validRExprInfArithOp :: ArithOp -> (RExpr, Type) -> (RExpr, Type) -> Position -> (RExpr, Type) 
validRExprInfArithOp Pow (r1,t1) (r2,t2) pos = e
   where
      e = (InfixOp (ArithOp Pow) e1 e2,t)
      t1' = validArithOpType Pow t1 pos $ " in expression \""++printTree r1++"\".\n"
      t = maxType t1' ti pos
      t2' = meetTypeRigid ti t2 pos $ " in expression \""++printTree r2++"\".\n"
      ti = BasicType BTInt
      e1 = (widenType t1 t r1, t1')
      e2 = (widenType t2 ti r2, t2')

validRExprInfArithOp Mod (r1,t1) (r2,t2) pos = e
   where
      e = (InfixOp (ArithOp Mod) e1 e2,ti)
      t1' = meetTypeRigid ti t1 pos $ " in expression \""++printTree r1++"\".\n"
      t2' = meetTypeRigid ti t2 pos $ " in expression \""++printTree r2++"\".\n"
      ti = BasicType BTInt
      e1 = (widenType t1 ti r1, t1')
      e2 = (widenType t2 ti r2, t2')
               
validRExprInfArithOp aOp (r1,t1) (r2,t2) pos = e
   where
      e = (InfixOp (ArithOp aOp) e1 e2,t)
      t1' = validArithOpType aOp t1 pos $ " in expression \""++printTree r1++ "\".\n"
      t2' = validArithOpType aOp t2 pos $ " in expression \""++printTree r2++ "\".\n"
      t = maxType t1' t2' pos
      e1 = (widenType t1 t r1, t1')
      e2 = (widenType t2 t r2, t2')

validRExprInfRelOp :: RelOp -> (RExpr, Type) -> (RExpr, Type) -> Position -> (RExpr, Type)
validRExprInfRelOp rOp (r1,t1) (r2,t2) pos = e
   where
      e = (InfixOp (RelOp rOp) e1 e2,tb)
      t = maxType t1 t2 pos
      tb = BasicType BTBool
      e1 = (widenType t1 t r1, t)
      e2 = (widenType t2 t r2, t)
               
validRExprInfBoolOp :: BoolOp -> (RExpr, Type) -> (RExpr, Type) -> Position -> (RExpr, Type)
validRExprInfBoolOp bOp (r1,t1) (r2,t2) pos = e
   where
      e = (InfixOp (BoolOp bOp) e1 e2,tb)
      tb = BasicType BTBool
      t1' = meetTypeRigid tb t1 pos $ " in expression \"("++printTree r1++ ")\".\n"
      t2' = meetTypeRigid tb t2 pos $ " in expression \"("++printTree r2++ ")\".\n"
      e1 = (r1, t1')
      e2 = (r2, t2')

--determina se l'espressione sia valida controllando che il tipo sia valido per l'operatore
-- altrimenti crea un type error
validRExprUnaryOp :: UnaryOp -> (RExpr, Type) -> Position -> (RExpr, Type) 
validRExprUnaryOp Not (re,te) pos = e
   where
      e = (UnaryOp Not r1,tb)
      tb = BasicType BTBool
      t1 = meetTypeRigid tb te pos $ " in expression \""++printTree re++"\".\n"
      r1 = (re, t1)

--determina se l'espressione sia valida controllando che il tipo sia valido per l'operatore
-- ed effettua, se necessario, una coertion del tipo
validRExprUnaryOp Neg (re, te) pos = e
   where
      e = (UnaryOp Neg r1,t)
      t1 = validUnaryOpType Neg te pos $ " in expression \""++printTree re++"\".\n"
      t = maxType t1 (BasicType BTChar) pos
      r1 = (widenType te t re,t1)

--controlla che la funzione chiamata sia dichiarata, che i tipi dei parametri siano corretti
-- ed eventualmente genera opportuni errori di tipo
validRExprFunCall :: Env -> Path -> DefVars -> Id -> [(RExpr, Type)] -> Position -> (RExpr, Type)
validRExprFunCall e pat defs i ats pos = case lookupFun e fi pat of
   [] -> (fun, TErr $ pos++undefFun)
   fs -> validFCall e pat defs i ats pos fs
   where
      fi = funIdent i ats
      fun = FCall i ats
      undefFun = " invalid call to an undefined function in \""++printTree fun++"\".\n"
      conpat = concat pat

validFCall :: Env -> Path -> DefVars -> Id -> [(RExpr,Type)] -> Position -> [FunInfo] -> (RExpr,Type)
validFCall env pat defs i ats pos fs = funi
   where
      (r:rs) = fs
      acc = aggr ats r
      (_,funi) = foldr (f ats) acc rs
      f att fi fc@(n,_)
         |nt <= n = (nt,fnew)
         |otherwise = fc
         where
            (nt,fnew) = aggr att fi 
      aggr att (FI ps t _ _) = (z,(FCall i zs, t))
         where
            zs = zipWith (checkParam env pat defs pos) ps ats
            z = parErr zs
            parErr = foldr p 0
            p (_,TErr _) n = n+1
            p _ n = n

checkParam :: Env -> Path -> DefVars -> Position -> Parameter -> (RExpr,Type) -> (RExpr,Type)
checkParam env pat defs pos (Param Reference i tp) (re, te) = case re of
   LExpr l -> r
      where
         r = (widenType te tp lr, tt)
         lr = LExpr ll
         ll = validRefParam env pat defs pos l
         tt = meetType tp te pos $ " in expression \""++printTree re++"\".\n"
   _ -> rm
      where 
         mod = pos++" formal parameter \""++printTree i++"\" has modality "++printTree Reference++
            ", while actual expression \""++printTree re++"\" is not a lexpr.\n"
         rm = (widenType te tp re, TErr mod)
               
checkParam _ _ _ pos (Param _ i tp) (re, te) = r
    where 
      r = (widenType te tp re, tt)
      tt = meetType tp te pos $ " in expression \""++printTree re++"\" bound to formal parameter "++printTree i++".\n"

validRefParam :: Env -> Path -> DefVars -> Position -> (LExpr,Type) -> (LExpr,Type)
validRefParam env pat defs pos l@((SId i _),te) = case lookupVar env i pat of
   [] -> l
   (x:_) -> f x
      where
         le = SId i
         f (VStatic _ _ _) = (le $ pos++" it is not possible to pass a static variable as a reference parameter in \""++printTree i++"\".\n",te)
         f (VConst _ _)
            |null def = (le $ pos++" variable \""++printTree i++"\" has been declared as constant and already initialized, thus it cannot be passed as a reference parameter.\n",te)
            |otherwise = (le "", te)
            where
               def = varDefined i pat defs pos
         f (VPar Constant _ _) = (le $ pos++" variable \""++printTree i++"\" has been declared as a constant parameter, thus it cannot be passed as a reference parameter.\n",te)
         f _ = (le "", te)
   
--controlla che la lexpr sia valida per l'operazione di reference, altrimenti associa un errore di tipo
validRef :: Env -> Path -> (LExpr,Type) -> Position -> (RExpr,Type)
validRef env pat l@(le,t) pos = (ref, typ)
   where
      ref = Ref l
      typ = validRefLExpr env pat t' le pos err
      err = " in the reference expression \""++printTree ref++"\".\n"
      t' = pointer t
      pointer e@(TErr _) = e
      pointer t = Pointer t

validRefLExpr env pat typ (Deref (LExpr (l,_),_)) pos err = validRefLExpr env pat typ l pos err
validRefLExpr env pat typ (Deref (_,_)) pos err = typ
validRefLExpr env pat typ (ArrayEl (l,_) _) pos err = validRefLExpr env pat typ l pos err
validRefLExpr env pat typ l@(SId i _) pos err = case lookupVar env i pat of
   [] -> typ
   (x:_) -> f x
      where
         f (VStatic _ _ _) = TErr $ pos++" it is not possible to get the reference of a variable declared as static in \""++printTree l++"\";"++err
         f _ = typ

validLExpr :: (LExpr,Type) -> (RExpr, Type)
validLExpr l@(_,t) = (LExpr l, t)

--controlla che l'applicazione del cast sia valida rispetto ai tipi,
-- in caso contrario restituisce un errore di tipo associato alla rexpr
validCast :: Type -> (RExpr,Type) -> Position -> (RExpr,Type)
validCast tc r@(re,te) pos = case te of
   TErr _ -> (Cast tc r,tc)
   _ -> (Cast tc (re,t),tc)
   where
      t = castType tc te pos $ " in the casting expression of \""++printTree re++"\".\n"

validTRExpr :: [(RExpr,Type)] -> (RExpr,Type)
validTRExpr rs = (TRExpr rs, Tuple ts)
   where
      ts = foldr f [] rs
      f (re,te) acc = te : acc

validArrRExpr :: [(RExpr,Type)] -> Position -> (RExpr,Type)
validArrRExpr [] _ = (ArrRExpr [], Array Nothing (BasicType BTUnit))
validArrRExpr a@(x:xs) pos = (ArrRExpr (x:as), Array len t1)
   where
      (_,t1) = x
      as = foldr (f pos t1) [] xs
      len = Just $ length a
      f p t (re,te) acc = (re,tt) : acc
         where
            tt = meetTypeRigid t te pos $ " in array element expression \""++printTree re++"\".\n"

--controlla che il break si trovi in una posizione corretta, altrimenti associa il relativo type error
validBreak :: Bool -> Position -> (RExpr,Type)
validBreak True _ = (Jmp Break, BasicType BTUnit)
validBreak _ pos  = (Jmp Break, TErr $ pos++" invalid use of break expression.\n") 

--controlla che il continue si trovi in una posizione corretta, altrimenti associa il relativo type error
validContinue :: Bool -> Position -> (RExpr,Type)
validContinue True _ = (Jmp Continue, BasicType BTUnit)
validContinue _ pos = (Jmp Continue, TErr $ pos++" invalid use of continue expression.\n")

--controlla che il return sia corretto rispetto al tipo di ritorno della funzione in cui è inserito
validReturnVoid :: Type -> Position -> (RExpr,Type)
validReturnVoid t@(BasicType BTUnit) _= (Jmp (RetExp (Const Unit,t)),t)
validReturnVoid t pos = (Jmp (RetExp (Const Unit,terr)),t)
   where
      terr = TErr $ pos++" expected function return type is "++printTree t++" while actual return type is ().\n"

--controlla che il return sia corretto rispetto al tipo di ritorno della funzione in cui è inserito
validReturn :: Type -> (RExpr, Type) -> Position -> (RExpr,Type)
validReturn t (re, te) pos = (Jmp (RetExp r), t)
    where
      t1 = meetType t te pos $ " in the function return expression \""++printTree re++"\".\n"
      r = (widenType te t re, t1)

validREBlk :: (Block,Type) -> (RExpr,Type)
validREBlk b@(_,tk) = (REBlk b,tk)

validBlock :: [Stmt] -> (RExpr,Type) -> (Block,Type)
validBlock ss r@(re,te) = (Block ss r, te)

validSel :: (IfRExpr, Type) -> (RExpr,Type)
validSel s@(_,ts) = (Sel s,ts)

--controlla che la guardia sia booleana e che il blocco abbia tipo unit
-- altrimenti associa opportuni errori di tipo
validIfNoElse :: (RExpr, Type) -> (Block,Type) -> Position -> (IfRExpr, Type)
validIfNoElse (re,te) (bk,tk) pos = iff
   where
      iff = (IfNoElse (re,t1) (bk,t2), tu)
      t1 = meetTypeRigid tb te pos $ "; the if guard type must be boolean in \""++printTree re++"\".\n"
      t2 = meetTypeRigid tu tk pos $ "; the if(no else) block type must be ().\n"
      tb = BasicType BTBool
      tu = BasicType BTUnit

--controlla che la guardia sia booleana e che i rami dell'if abbiano lo stesso tipo
-- altrimenti associa opportuni errori di tipo
validIfElse :: (RExpr, Type) -> (Block,Type) -> (ElseBlock,Type) -> Position -> (IfRExpr, Type)
validIfElse (re,te) (bk,tk) (ek,et) pos = iff
   where
      iff = (IfElse (re,t1) (bk,tk) (ek,t2), tk)
      t1 = meetTypeRigid tb te pos $ "; the if guard type must be boolean in \""++printTree re++"\".\n"
      t2 = meetTypeRigid tk et pos $ "; the branches type of an if(else) expression must be the same.\n"
      tb = BasicType BTBool

validEBlk :: (Block,Type) -> (ElseBlock, Type)
validEBlk b@(_,tk) = ebl
   where
      ebl = (EBlk b, tk)

validEIf :: (IfRExpr, Type) -> (ElseBlock, Type)
validEIf ife@(_,te) = ebl
   where
      ebl = (EIf ife, te)

--controlla che la guardia sia booleana e che il blocco abbia tipo unit
-- altrimenti associa opportuni errori di tipo
validWhile :: (RExpr, Type) -> (Block,Type) -> Position -> (RExpr, Type)
validWhile (re,te) (bk,tk) pos = wh
   where
      wh = (Iter (While (re,t1) (bk,t2)), tu)
      t1 = meetTypeRigid tb te pos $ "; the while guard type must be boolean in \""++printTree re++"\".\n"
      t2 = meetTypeRigid tu tk pos $ "; the while block type must be ().\n"
      tb = BasicType BTBool
      tu = BasicType BTUnit

--controlla che il blocco abbia tipo unit altrimenti associa un errore di tipo
validLoop :: (Block,Type) -> Position -> (RExpr, Type)
validLoop (bk,tk) pos = wh
   where
      wh = (Iter (Loop (bk,t1)), tu)
      t1 = meetTypeRigid tu tk pos $ "; the loop block type must be ().\n"
      tu = BasicType BTUnit

validDeref :: (RExpr, Type) -> Position -> (LExpr,Type)
validDeref d@(re,te) pos = (Deref d, t)
   where
      t = unPointer te $ pos++" expression \""++printTree re++"\" is not a pointer type.\n"
      unPointer (Pointer tp) _ = tp
      unPointer _ err = TErr err

--controlla che l'indice dell'array sia di tipo intero che il tipo del lexpr sia array
-- in caso contrario associa opportuni errori di tipo
validArrayEl :: (LExpr,Type) -> (RExpr,Type) -> Position -> (LExpr,Type)
validArrayEl ll@(l,t) (r,t1) pos = (ArrayEl ll r', tt)
   where
      ti = BasicType BTInt
      t' = meetType ti t1 pos $ " in array index expression \""++printTree r++"\"\n."
      r' = (widenType t1 ti r, t')
      tt = unArray t $ pos++" expression \""++printTree l++"\" is not an array.\n"
      unArray (Array _ ta) _ = ta
      unArray _ err = TErr err

--controlla che la variabile sia stata dichiarata ed inizializzata
rExprCheck :: Path -> Id -> DefVars -> Env -> Position -> (LExpr,Type)
rExprCheck pat i ds e pos = case lookupVar e i pat of
   [] -> (l, TErr err)
   (x:_) -> aggr x
   where
      l = SId i def
      def = varDefined i pat ds pos
      err = pos++" variable \""++printTree i++"\" is not declared.\n"
      aggr x = (l,t)
         where
            t = vType err x

--controlla che la variabile sia stata dichiarata e che non sia stata dichiarata come costante
assgnCheck :: AssignmentOp -> Path -> Id -> DefVars -> Env -> Position -> (LExpr,Type)
assgnCheck Assign pat i ds e pos = case lookupVar e i pat of
   [] -> (l "", TErr err2)
   (x:_) -> aggr x
   where
      l = SId i
      err = pos++" on the left side of the assignment the specified variable \""++printTree i++"\""
      err2 = err++" is not declared.\n"
      aggr x = (l e, t)
         where
            t = vType err2 x
            e = validLHSVarInfo x i pat ds err
      
--controlla che la variabile sia stata dichiarata, inizializzata e che non sia stata dichiarata come costante
assgnCheck aOp pat i ds e pos = case lookupVar e i pat of
   [] -> (l def, TErr err2)
   (x:_) -> aggr x
   where
      l = SId i
      err = pos++" on the left side of the assignment ("++printTree aOp++") the specified variable \""++printTree i++"\""
      err2 = err++" is not declared.\n"
      def = varDefined i pat ds pos
      aggr x = (l $ e++def, t)
         where
            t = vType err2 x
            e = validLHSVarInfo x i pat ds err

--controlla se sia valido effettuare un assegnamento sulla variabile specificata;
-- nel caso in cui la variabile sia stata dichiarata come costante, si controlla che non sia già stata inizializzata,
-- altrimenti si segnala l'errore;
--nel caso in cui sia stata dichiara come static, si genera l'errore dato che la variabile risulta essere inizializzata;
-- nel caso in cui sia un parametro formale, si controlla se sia stata dichiarata come costante, in tal caso si segnala l'errore.
validLHSVarInfo :: VarInfo -> Id -> Path -> DefVars -> Error-> Error
validLHSVarInfo (VConst _ _) i pat dv err 
   |null def = err++" has been declared as constant and already initialized.\n"
   |otherwise = ""
   where
      def = varDefined i pat dv err
      
validLHSVarInfo (VStatic _ _ _) _ _ _ err = err++" has been declared as static, thus it cannot be modified.\n" 
validLHSVarInfo (VPar Constant _ _) _ _ _ err = err++" has been declared as a costant parameter.\n"
validLHSVarInfo _ _ _ _ err = ""

--controlla che la variabile sia stata inizializzata, altrimenti genera una messaggio di errore
varDefined :: Id -> Path -> DefVars -> Position -> Error
varDefined i pat dv pos = case filter p dv of
   [] -> pos++" variable \""++printTree i++"\" is never initialized.\n"
   _ -> ""
   where
      p (idv,pt) = i == idv && lp >= lpt
         where
            lp = length pat
            lpt = length pt
      
